(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
dbl(S(0), S(0)) → S(S(S(S(0))))
save(S(x)) → dbl(0, save(x))
save(0) → 0
dbl(0, y) → y
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
S0(0) → 0
00() → 0
dbl0(0, 0) → 1
save0(0) → 2
01() → 5
S1(5) → 4
S1(4) → 3
S1(3) → 3
S1(3) → 1
01() → 6
save1(0) → 7
dbl1(6, 7) → 2
01() → 2
dbl1(6, 7) → 7
01() → 7
0 → 1
7 → 2
(2) BOUNDS(1, n^1)